M:MsgA, k:Knd, s:M.state, v:M.da(k). M.sends(k,s,v)  M.Msg List 

latex

Definitions	P  Q, P & Q, P  Q, P  Q, x(s1,s2), Msg(M), mlnk(m), M.sends(k,s,v), MsgA, M.state, M.da(a), M.Msg, concat(ll), map(f;as), fpf-vals(eq;P;f), product-deq(A;B;a;b), IdLnkDeq, eqof(d), 1of(t), , x. t(x), KindDeq, x:A. B(x), tagged-messages(l;s;v;L), 2of(t), rcv(l,tg), Valtype(da;k), Id, b, IdLnk, f(x)?z, Top, Knd, State(ds), Msg(da), t  T
Lemmas	Knd wf, ma-state wf, top wf, Kind-deq wf, fpf-cap wf, pi1 wf, eqof wf, pi2 wf, rcv wf, ma-valtype wf, Id wf, idlnk-deq wf, product-deq wf, fpf-vals wf, assert wf, IdLnk wf, map wf, ma-Msg wf, concat wf, msga wf, tagged-messages wf, deq property, mlnk wf, Msg wf, subtype rel list